-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add BoundedInts to DafnyStdLibs #4713
Add BoundedInts to DafnyStdLibs #4713
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great and I like the testing approach! Just a couple of thoughts for later and a question.
@@ -1,172 +1,168 @@ | |||
module Demo { | |||
import opened DafnyStdLibs.Wrappers |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good change, but wow did GitHub ever mess up the diff something terrible. :)
|
||
module {:extern} Externs { | ||
import opened DafnyStdLibs.BoundedInts | ||
class {:extern} NonDefault { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why "NonDefault"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My impression is that for Java an extern should not be in the default class since there are no partial classes.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh Java does support mixed Dafny and target classes: https://github.com/dafny-lang/dafny/blob/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Mixed.java And that works fine with default classes, it just looks weird because of the __default
name.
This way is just fine though, I just didn't get why the class was named what it was.
$(DAFNY) test -t:cs build/stdlibexamples.doo examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples | ||
$(DAFNY) test -t:java build/stdlibexamples.doo examples/BoundedInts/Externs/NonDefault.java --output:build/stdlibexamples | ||
$(DAFNY) test -t:go build/stdlibexamples.doo examples/BoundedInts/NonDefault.go --output:build/stdlibexamples | ||
$(DAFNY) test -t:py build/stdlibexamples.doo examples/BoundedInts/NonDefault.py --output:build/stdlibexamples | ||
$(DAFNY) test -t:js build/stdlibexamples.doo examples/BoundedInts/NonDefault.js --output:build/stdlibexamples |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fine for this change but probably worth replacing with a find
of all files of the right extension in the next one, and before too long with project file support for this. :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Or look into target specific options in the project file
Almost forgot, make sure you update https://github.com/dafny-lang/dafny/tree/master/Source/DafnyStandardLibraries#available-libraries too! Might be worth adding a tiny |
567ada9
to
6f032e3
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just a few more nits, nothing hard-blocking. Happy with the {:dummyImportMember}
name. Do update the PR description so the commit message is accurate. :)
|
||
module {:extern} Externs { | ||
import opened DafnyStdLibs.BoundedInts | ||
class {:extern} NonDefault { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh Java does support mixed Dafny and target classes: https://github.com/dafny-lang/dafny/blob/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Mixed.java And that works fine with default classes, it just looks weird because of the __default
name.
This way is just fine though, I just didn't get why the class was named what it was.
@@ -2,7 +2,7 @@ | |||
// RUN: %exits-with 3 %dafny /compile:3 /unicodeChar:0 /spillTargetCode:2 "%s" /compileTarget:go 2> "%t" | |||
// note: putting /compileTarget:go after "%s" overrides user-provided option | |||
// RUN: %OutputCheck --file-to-check "%t" "%s" | |||
// CHECK: GoModuleConversions.go:10:3: "net/url" imported and not used | |||
// CHECK: undefined: GoModuleConversions.ParseURL |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not clear on why this is the error we're getting now, but not a blocker since this is just a negative test.
} else { | ||
isType = true; | ||
if (import.ExternModule != null) { | ||
var attributes = Attributes.Find(import.ExternModule.Attributes, "dummyImportMember"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Definitely glad we're not documenting this officially, but it might be worth adding a note on this attribute to https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/CONTRIBUTING.md, just so anyone that might need to use it is at least aware of how it works.
@@ -167,12 +167,14 @@ public abstract class SinglePassCompiler { | |||
/// call to the instance Main method in the enclosing class. | |||
/// </summary> | |||
protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr, string argsParameterName); | |||
protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr); | |||
protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Definitely feels a little weird to have a parameter that is "the module being created, but only passed if it's an extern". Consider keeping isExtern
and theModule
as separate parameters.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just for my own understanding, are the AST changes unrelated cleanup or necessary somehow?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unrelated, yes
Description
BoundedInts.dfy
,BoundedInts.md
andBoundedIntExamples.dfy
from https://github.com/dafny-lang/libraries to https://github.com/dafny-lang/dafny/tree/master/Source/DafnyStandardLibraries{:extern}
module, using a new undocumented, only internally used,{:member <name>, <isType>}
attribute. This is necessary to let theBoundedIntExamples.dfy
pass, becauseFunctionExamples.dfy
, which is part of the same project, does not use the{:extern}
module, so Go gives an unused import error. In the future I expect that we change our Go compiler so it only emits imports that are used, which makes the{:member}
attribute obsolete and allows us to remove support for it from our codebase without breaking anyone.How has this been tested?
int32
in Dafny.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.